\begin{tabbing}
$\forall$${\it es}$:ES, $X$:AbsInterface(Top), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ le($X$)))
\\[0ex]$\Rightarrow$ \=(le($X$)($e$) $\leq$loc $e$ \+
\\[0ex]\& ($\uparrow$(le($X$)($e$) $\in_{b}$ $X$))
\\[0ex]\& ($\forall$${\it e''}$:E. ${\it e''}$ $\leq$loc $e$  $\Rightarrow$ (le($X$)($e$) $<$loc ${\it e''}$) $\Rightarrow$ ($\neg$($\uparrow$(${\it e''}$ $\in_{b}$ $X$)))))
\-
\end{tabbing}